a, b:, n:. (a < b)  ((n * a) < (n * b)) 

latex

Up	int 2, int 2
Definitions	, t  T, P  Q, x:A. B(x), False, A, P  Q, Dec(P), , P & Q, {T}, P  Q, A  B
Lemmas	nat plus wf, decidable int equal, nat plus properties, lt to le rw, add functionality wrt le